d-world(D;v;sched;dec)
== <(i,x. M(i).ds(x))
== ,(i,a. M(i).da(locl(a)))
== ,(l,tg. M(source(l)).dout(l,tg))
== ,(i,t. if t=0 x.M(i).init(x)?v(i,x) else 1of(CV(d-comp(D;v;sched;dec))(t-1,i)) fi)
== ,(i,t. 1of(2of(CV(d-comp(D;v;sched;dec))(t,i))))
== ,(i,t. 2of(2of(CV(d-comp(D;v;sched;dec))(t,i))))
== ,(i.d-machine(i;M(i);dec(i)))
== ,> 

latex

---

clarification:

d-world{i:l}
d-world(D; v; sched; dec)
== <(i,x. d-m(D; i).ds(x))
== ,(i,a. d-m(D; i).da(locl(a)))
== ,(l,tg. d-m(D; source(l)).dout(l,tg))
== ,(i,t. if t=0 x.d-m(D; i).init(x)?v(i,x) else 1of(CV(d-comp(D;v;sched;dec))(t-1,i)) fi)
== ,(i,t. 1of(2of(CV(d-comp(D;v;sched;dec))(t,i))))
== ,(i,t. 2of(2of(CV(d-comp(D;v;sched;dec))(t,i))))
== ,(i.d-machine(i;d-m(D; i);dec(i)))
== ,> 

latex

Definitions	M.ds(x), M.da(a), locl(a), M.dout(l,tg), source(l), if b t else f fi, i=j, M.init(x)?v, n-m, #$n, 1of(t), 2of(t), CV(F), d-comp(D;v;sched;dec), <a,b>, x.A(x), d-machine(i;M;dec), M(i), f(a),
FDL editor aliases	d-world